Inference at * 
Iof proof for Lemma length of not nil:


  A:Type, as:(A List). ((as = []))  (||as||  1 ) 

latex

 by ((((((RepD) 
CollapseTHENM (OnVar `as' D))) 
CollapseTHENM (Reduce 0))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. A : Type
C1: 2. ([] = [])
C1:   0  1 
C2: 

C2: 1. A : Type
C2: 2. u : A
C2: 3. v : A List
C2: 4. ([u / v] = [])
C2:   (||v||+1)  1 
C3: 

C3: 1. A : Type
C3: 2. u : A
C3: 3. v : A List
C3: 4. (||v||+1)  1 
C3:   ([u / v] = [])
C.

Definitions	False, , t  T, P  Q, P  Q, P & Q, Y, ||as||, A, P  Q, x:A. B(x), A  B, i  j
Lemmas	length wf1, ge wf, not wf